es:ES, p:(E(E + Top)).
(causal-predecessor(es;p) & p-inject(E;E;p))
 (e, e':E. same-thread(es;p;e;e')  ((e p< e'  (e = e'))  e' p< e)) 

latex

Definitions	, x:A. B(x), e p< e', P  Q, e p e', {T}, SQType(T), , t  T, P & Q, P  Q, x:A. B(x), e c e', False, A  B, A, A c B, outl(x), isl(x), tt, (i = j), if b then t else f fi , Y, do-apply(f;x), p-id(), primrec(n;b;c), can-apply(f;x), b, f^n, p-graph(A;f), Dec(P), , S  T, same-thread(es;p;e;e')
Lemmas	decidable es-E-equal, es-causle weakening p-le, nat plus inc, p-fun-exp wf, p-graph wf2, es-p-locl wf, decidable int equal, causal-pred-wellfounded, same-final-iterate-one-one, event system wf, top wf, p-inject wf, causal-predecessor wf, es-E wf, same-thread wf